\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, $L$:IdLnk List, $T$:(Id$\rightarrow$Type).
\\[0ex]es{-}secret{-}server\=\{table:ut2, encrypt:ut2, decrypt:ut2\}\+
\\[0ex](${\it es}$; $T$; $L$; $i$)
\-\\[0ex]$\Rightarrow$ \=$\forall$$e_{1}$@$i$.\+
\\[0ex]$\forall$$e_{2}$@$i$.
\\[0ex]$\forall$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$"table" when $e_{1}$$\parallel$ }}$, $m$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$"table" when $e_{2}$$\parallel$ }}$.
\\[0ex]st{-}atom("table" when $e_{1}$;$n$) $=$ st{-}atom("table" when $e_{2}$;$m$) $\in$ Atom1 $\Rightarrow$ $n$ $=$ $m$ $\in$ $\mathbb{Z}$
\-
\end{tabbing}